Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar3/variousSLASH04.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1₅(h1, h2, x, y, z) -> e2₅(x, x, y, z, z)
e1₅(x1, x1, x, y, z) -> e5₄(x1, x, y, z)
e2₅(f1, x, y, z, f2) -> e3₁₁(x, y, x, y, y, z, y, z, x, y, z)
e2₅(x, x, y, z, z) -> e6₃(x, y, z)
e2₅(i, x, y, z, i) -> e6₃(x, y, z)
e3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e3₁₁(x, y, x, y, y, z, y, z, x, y, z) -> e6₃(x, y, z)
e4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1₅(x1, x1, x, y, z)
e4₁₁(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5₄(x1, x, y, z)
e4₁₁(x, x, x, x, x, x, x, x, x, x, x) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1₅(h1, h2, x, y, z) -> e2₅(x, x, y, z, z)
e1₅(x1, x1, x, y, z) -> e5₄(x1, x, y, z)
e2₅(f1, x, y, z, f2) -> e3₁₁(x, y, x, y, y, z, y, z, x, y, z)
e2₅(x, x, y, z, z) -> e6₃(x, y, z)
e2₅(i, x, y, z, i) -> e6₃(x, y, z)
e3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e3₁₁(x, y, x, y, y, z, y, z, x, y, z) -> e6₃(x, y, z)
e4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1₅(x1, x1, x, y, z)
e4₁₁(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5₄(x1, x, y, z)
e4₁₁(x, x, x, x, x, x, x, x, x, x, x) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

F1 -> G2
F2 -> G1
E2₅(f1, x, y, z, f2) -> E3₁₁(x, y, x, y, y, z, y, z, x, y, z)
G1 -> H2
G2 -> H1
E1₅(x1, x1, x, y, z) -> E5₄(x1, x, y, z)
E1₅(h1, h2, x, y, z) -> E2₅(x, x, y, z, z)
G1 -> H1
F2 -> G2
G2 -> H2
E3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E4₁₁(i, x1, i, x1, i, x1, i, x1, x, y, z) -> E5₄(x1, x, y, z)
F1 -> G1
E4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E1₅(x1, x1, x, y, z)

The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1₅(h1, h2, x, y, z) -> e2₅(x, x, y, z, z)
e1₅(x1, x1, x, y, z) -> e5₄(x1, x, y, z)
e2₅(f1, x, y, z, f2) -> e3₁₁(x, y, x, y, y, z, y, z, x, y, z)
e2₅(x, x, y, z, z) -> e6₃(x, y, z)
e2₅(i, x, y, z, i) -> e6₃(x, y, z)
e3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e3₁₁(x, y, x, y, y, z, y, z, x, y, z) -> e6₃(x, y, z)
e4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1₅(x1, x1, x, y, z)
e4₁₁(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5₄(x1, x, y, z)
e4₁₁(x, x, x, x, x, x, x, x, x, x, x) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F1 -> G2
F2 -> G1
E2₅(f1, x, y, z, f2) -> E3₁₁(x, y, x, y, y, z, y, z, x, y, z)
G1 -> H2
G2 -> H1
E1₅(x1, x1, x, y, z) -> E5₄(x1, x, y, z)
E1₅(h1, h2, x, y, z) -> E2₅(x, x, y, z, z)
G1 -> H1
F2 -> G2
G2 -> H2
E3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E4₁₁(i, x1, i, x1, i, x1, i, x1, x, y, z) -> E5₄(x1, x, y, z)
F1 -> G1
E4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E1₅(x1, x1, x, y, z)

The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1₅(h1, h2, x, y, z) -> e2₅(x, x, y, z, z)
e1₅(x1, x1, x, y, z) -> e5₄(x1, x, y, z)
e2₅(f1, x, y, z, f2) -> e3₁₁(x, y, x, y, y, z, y, z, x, y, z)
e2₅(x, x, y, z, z) -> e6₃(x, y, z)
e2₅(i, x, y, z, i) -> e6₃(x, y, z)
e3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e3₁₁(x, y, x, y, y, z, y, z, x, y, z) -> e6₃(x, y, z)
e4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1₅(x1, x1, x, y, z)
e4₁₁(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5₄(x1, x, y, z)
e4₁₁(x, x, x, x, x, x, x, x, x, x, x) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 10 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

E1₅(h1, h2, x, y, z) -> E2₅(x, x, y, z, z)
E3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E1₅(x1, x1, x, y, z)
E2₅(f1, x, y, z, f2) -> E3₁₁(x, y, x, y, y, z, y, z, x, y, z)

The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e1₅(h1, h2, x, y, z) -> e2₅(x, x, y, z, z)
e1₅(x1, x1, x, y, z) -> e5₄(x1, x, y, z)
e2₅(f1, x, y, z, f2) -> e3₁₁(x, y, x, y, y, z, y, z, x, y, z)
e2₅(x, x, y, z, z) -> e6₃(x, y, z)
e2₅(i, x, y, z, i) -> e6₃(x, y, z)
e3₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e4₁₁(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e3₁₁(x, y, x, y, y, z, y, z, x, y, z) -> e6₃(x, y, z)
e4₁₁(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e1₅(x1, x1, x, y, z)
e4₁₁(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e5₄(x1, x, y, z)
e4₁₁(x, x, x, x, x, x, x, x, x, x, x) -> e6₃(x, x, x)
e5₄(i, x, y, z) -> e6₃(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.